(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (exists ((d Int)) (> (/ 0.0 (+ 0.5 (ite (distinct a d) b c))) 0)))
(check-sat)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (exists ((c Int)) (> (/ (+ c 1) (+ 0.5 (ite (= c 2) a b))) 2)))
(check-sat)
(declare-fun a () Real)
(declare-fun b () Int)
(assert (and (> a 1) (= 0 (/ 1 a b))))
(check-sat)
(assert (exists ((a Real) (b Real)) (and (= a 2) (or (= (/ 1 a) 0) (> b 0)))))
(check-sat)
